The present disclosure relates to solving a Boolean satisfiability problem (SAT), also referred to as SAT solving, in general, and to SAT solving of Bounded Model Checking (BMC) problem in particular.
Computerized devices are an important part of the modern life. They control almost every aspect of our life—from writing documents to controlling traffic lights. However, computerized devices are bug-prone, and thus require a verification phase in which the bugs should be discovered. The verification phase is considered one of the most difficult tasks in developing a computerized device. Many developers of computerized devices invest a significant portion, such as 70%, of the development cycle to discover erroneous behaviors of the computerized device, also referred to as a target computerized system. The target computerized system may comprise hardware, software, firmware, a combination thereof and the like.
During the verification phase model checking techniques may be utilized to verify that a property is held by the target computerized system. The target computerized system is represented using a model, defining a state of the target computerized system in each cycle. The state may be affected by a state in a previous cycle, an input to the model, a nondeterministic decision or the like. Some model checking techniques, such as Bounded Model Checking (BMC), utilize a SAT solver. In order to utilize a SAT solver, the model is reduced to a corresponding formula which may be represented by a Conjunctive Normal Form (CNF) formula. A CNF formula comprises of a conjunction of clauses. Each clause comprises a disjunction of literals. Each literal is associated with a Boolean variable and a truth value. The CNF formula may comprise clauses corresponding to constraints associated with an initial state of the model. The CNF formula may comprise clauses corresponding to constraints associated with a verified property checked in the model. The CNF formula may comprise clauses corresponding to transition relation of the model, corresponding to a change between a state and a next state.